\begin{tabbing} $\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+ \\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)\} . \-\\[0ex]$x$ changed before $e$ $\in$ $\mathbb{B}$ \end{tabbing}